1. Technical Field
The present invention relates to model checking methods and systems, and more particularly to verifying the precision of programs employing floating point operations.
2. Description of the Related Art
With the growth of multi-core processing and concurrent programming in many key computing segments, as utilized in mobile, server and gaming technologies, effective development and verification tools for concurrent multi-threaded programs have been sought after. At the same time, due to the ubiquitous availability of real-time and cyber-systems that interact with physical environments, there is a great need to develop technologies that target the whole system. Analyzing software for its correctness is a key step in guaranteeing safety of many important real-time and embedded devices, such as medical devices and devices employed in automobiles or airplanes.
Recently, there has been extensive research on model checking software programs. All of these techniques attempt to cover as many different language features as possible, but lately the focus has been on memory correctness issues due to intricate use of pointer indirections, for example. The only model checking tools known to the inventors that handle floating-point operations are based on the CProver infrastructure in accordance with a CBMC (Bounded Model Checker for ANSI-C (American National Standards Institute for C Programming) and C++ programs) and SATABS (SAT (Boolean satisfiability problem)-based Predicate Abstraction). The tool generates a bit-blasted formula for floating-point computations that is translated directly to a SAT solver in the backend. Further, the floating point handling in CBMC has been improved by using counterexample-guided mixed over- and under-approximations when analyzing the bit-blasted formula.
In addition, there are several tools based on abstract interpretation that target the ever growing embedded software domain. These tools focus mostly on floating-point semantics, given their prevalence and importance for the safety of embedded software, such as that used in medical devices, cars, airplanes and so on. These tools include ASTREE (real-time embedded software static analyzer), FLUCTUAT, and PolySpace. Moreover, these tools provide scalable analysis techniques based on abstract interpretation by limiting precision in certain cases, for example due to widening of loops.